| Definitions | f(x)?z, A c B, p  q, let x = a in b(x), Normal(ds),  x dom(f). v=f(x)   P(x;v), Realizer, Rsends-T(x1), Reffect-T(x1), Rsends-dt(x1), R-interface-compat(A;B), Rinit-v(x1), Rinit-discrete(A), Rinit-x(x1), Rinit?(x1), Reffect-f(x1), Reffect-discrete(A), R-discrete_compat(A;B), Rpre-a(x1), Rpre-ds(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-knd(x1), Rsends-g(x1), Rsframe-tag(x1), Rsends-l(x1), Rsframe-lnk(x1), Rsframe?(x1), Rsends?(x1), Rrframe-L(x1), Reffect-ds(x1), Rrframe-x(x1), Rrframe?(x1), outl(x),  T, do-apply(f;x), can-apply(f;x), Raframe-L(x1), Raframe-k(x1), Raframe?(x1), isl(x), Rframe-L(x1), Reffect-knd(x1), Reffect-x(x1), Rframe-x(x1), Rframe?(x1), Reffect?(x1), R-frame-compat(A;B), suptype(S; T), S  T,   x,y. t(x;y), (i = j), p  q, R-base-domain(R), R-loc(R), R-FeasibleWitness, base-domain-type(n), Rda(R), {T}, SQType(T), x : v, t.2, x. t(x), t.1, f(x), Rds(R), Rnone?(x1), Rplus?(x1),  b, f || g, i  j , False,  A, A  B, ff, tt, True, P & Q, if b then t else f fi , Y,  , t T, A || B, P Q, Top, x:A. B(x), xL. P(x), ||as||, x(s1,s2), P Q, reduce(f;k;as), deq-member(eq;x;L),  , x(s), x dom(f),  , P  Q, Unit,  ,  , Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, Rnone(),  , fpf-domain(f) |
| Lemmas | lnk-decl-ap, lnk-decl-dom, isrcv-implies, fpf-ap wf, assert-eq-lnk, bool sq, Rinit? wf, Rpre? wf, Rbframe? wf, IdLnk sq, Rsframe? wf, member-fpf-dom, Rrframe? wf, outl wf, squash wf, Raframe? wf, bfalse wf, btrue wf, cons one one, non neg length, length wf nat, Rsends? wf, Rframe? wf, Reffect? wf, assert-eq-bd, p-outcome wf, map wf, normal-ds wf, tagof wf, fpf-cap wf, eq lnk wf, do-apply wf, can-apply wf, fpf-domain wf, l all wf2, l member wf, lnk wf, ldst wf, isrcv wf, fpf-all wf, pi2 wf, lsrc wf, isl wf, R-base-domain wf, eq bd wf, assert of bor, lnk-decl wf, fpf-join-dom-sq, locl wf, fpf-single wf, fpf-join-ap-sq, Knd sq, Rda wf, Kind-deq wf, Rrframe wf, Rbframe wf, Raframe wf, Rpre wf, Rsends wf, Reffect wf, Rsframe wf, Rframe wf, fpf-trivial-subtype-top, Rinit wf, Rds wf, pi1 wf, Id sq, fpf-single-dom, Rplus wf, Rnone wf, false wf, true wf, id-deq wf, fpf-dom wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, unit wf, not functionality wrt iff, assert-eq-id, ge wf, nat properties, R-loc wf, eq id wf, Rnone? wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, Rplus-right wf, R-size-decreases, Rplus-left wf, R-FeasibleWitness-Rplus, Rplus-implies, eqtt to assert, Rplus? wf, le wf, rationals wf, bool wf, base-domain-type wf, Id wf, IdLnk wf, top wf, Knd wf, es realizer wf, R-FeasibleWitness wf, nat plus wf, R-size wf, nat wf |
(T:Type 
(T + (
cl:(Id